0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 4 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇒, 37 ms)
↳8 QDP
↳9 Narrowing (⇔, 11 ms)
↳10 QDP
↳11 Instantiation (⇔, 0 ms)
↳12 QDP
↳13 Instantiation (⇔, 0 ms)
↳14 QDP
↳15 QDPOrderProof (⇔, 170 ms)
↳16 QDP
↳17 DependencyGraphProof (⇔, 0 ms)
↳18 TRUE
hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → DISTR_IN_GGAA(s(X), X, DL, DR)
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_GA(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)
hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → DISTR_IN_GGAA(s(X), X, DL, DR)
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_GA(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)
hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)
hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))
U1_GA(distr_out_ggaa(DL, DR)) → U2_GA(DR, hbal_tree_in_ga(DL))
U2_GA(DR, hbal_tree_out_ga(L)) → HBAL_TREE_IN_GA(DR)
HBAL_TREE_IN_GA(s(s(X))) → U1_GA(distr_in_ggaa(s(X), X))
U1_GA(distr_out_ggaa(DL, DR)) → HBAL_TREE_IN_GA(DL)
hbal_tree_in_ga(zero) → hbal_tree_out_ga(nil)
hbal_tree_in_ga(s(zero)) → hbal_tree_out_ga(t(x, nil, nil))
hbal_tree_in_ga(s(s(X))) → U1_ga(distr_in_ggaa(s(X), X))
distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D2, D1)
U1_ga(distr_out_ggaa(DL, DR)) → U2_ga(DR, hbal_tree_in_ga(DL))
U2_ga(DR, hbal_tree_out_ga(L)) → U3_ga(L, hbal_tree_in_ga(DR))
U3_ga(L, hbal_tree_out_ga(R)) → hbal_tree_out_ga(t(x, L, R))
hbal_tree_in_ga(x0)
distr_in_ggaa(x0, x1)
U1_ga(x0)
U2_ga(x0, x1)
U3_ga(x0, x1)
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), s(x1)))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), x1))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(x1, s(x1)))
U1_GA(distr_out_ggaa(DL, DR)) → U2_GA(DR, hbal_tree_in_ga(DL))
U2_GA(DR, hbal_tree_out_ga(L)) → HBAL_TREE_IN_GA(DR)
U1_GA(distr_out_ggaa(DL, DR)) → HBAL_TREE_IN_GA(DL)
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), s(x1)))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), x1))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(x1, s(x1)))
hbal_tree_in_ga(zero) → hbal_tree_out_ga(nil)
hbal_tree_in_ga(s(zero)) → hbal_tree_out_ga(t(x, nil, nil))
hbal_tree_in_ga(s(s(X))) → U1_ga(distr_in_ggaa(s(X), X))
distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D2, D1)
U1_ga(distr_out_ggaa(DL, DR)) → U2_ga(DR, hbal_tree_in_ga(DL))
U2_ga(DR, hbal_tree_out_ga(L)) → U3_ga(L, hbal_tree_in_ga(DR))
U3_ga(L, hbal_tree_out_ga(R)) → hbal_tree_out_ga(t(x, L, R))
hbal_tree_in_ga(x0)
distr_in_ggaa(x0, x1)
U1_ga(x0)
U2_ga(x0, x1)
U3_ga(x0, x1)
U1_GA(distr_out_ggaa(s(z0), s(z0))) → U2_GA(s(z0), hbal_tree_in_ga(s(z0)))
U1_GA(distr_out_ggaa(s(z0), z0)) → U2_GA(z0, hbal_tree_in_ga(s(z0)))
U1_GA(distr_out_ggaa(z0, s(z0))) → U2_GA(s(z0), hbal_tree_in_ga(z0))
U2_GA(DR, hbal_tree_out_ga(L)) → HBAL_TREE_IN_GA(DR)
U1_GA(distr_out_ggaa(DL, DR)) → HBAL_TREE_IN_GA(DL)
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), s(x1)))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), x1))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(x1, s(x1)))
U1_GA(distr_out_ggaa(s(z0), s(z0))) → U2_GA(s(z0), hbal_tree_in_ga(s(z0)))
U1_GA(distr_out_ggaa(s(z0), z0)) → U2_GA(z0, hbal_tree_in_ga(s(z0)))
U1_GA(distr_out_ggaa(z0, s(z0))) → U2_GA(s(z0), hbal_tree_in_ga(z0))
hbal_tree_in_ga(zero) → hbal_tree_out_ga(nil)
hbal_tree_in_ga(s(zero)) → hbal_tree_out_ga(t(x, nil, nil))
hbal_tree_in_ga(s(s(X))) → U1_ga(distr_in_ggaa(s(X), X))
distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D2, D1)
U1_ga(distr_out_ggaa(DL, DR)) → U2_ga(DR, hbal_tree_in_ga(DL))
U2_ga(DR, hbal_tree_out_ga(L)) → U3_ga(L, hbal_tree_in_ga(DR))
U3_ga(L, hbal_tree_out_ga(R)) → hbal_tree_out_ga(t(x, L, R))
hbal_tree_in_ga(x0)
distr_in_ggaa(x0, x1)
U1_ga(x0)
U2_ga(x0, x1)
U3_ga(x0, x1)
U1_GA(distr_out_ggaa(s(z0), s(z0))) → HBAL_TREE_IN_GA(s(z0))
U1_GA(distr_out_ggaa(s(z0), z0)) → HBAL_TREE_IN_GA(s(z0))
U1_GA(distr_out_ggaa(z0, s(z0))) → HBAL_TREE_IN_GA(z0)
U2_GA(DR, hbal_tree_out_ga(L)) → HBAL_TREE_IN_GA(DR)
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), s(x1)))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), x1))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(x1, s(x1)))
U1_GA(distr_out_ggaa(s(z0), s(z0))) → U2_GA(s(z0), hbal_tree_in_ga(s(z0)))
U1_GA(distr_out_ggaa(s(z0), z0)) → U2_GA(z0, hbal_tree_in_ga(s(z0)))
U1_GA(distr_out_ggaa(z0, s(z0))) → U2_GA(s(z0), hbal_tree_in_ga(z0))
U1_GA(distr_out_ggaa(s(z0), s(z0))) → HBAL_TREE_IN_GA(s(z0))
U1_GA(distr_out_ggaa(s(z0), z0)) → HBAL_TREE_IN_GA(s(z0))
U1_GA(distr_out_ggaa(z0, s(z0))) → HBAL_TREE_IN_GA(z0)
hbal_tree_in_ga(zero) → hbal_tree_out_ga(nil)
hbal_tree_in_ga(s(zero)) → hbal_tree_out_ga(t(x, nil, nil))
hbal_tree_in_ga(s(s(X))) → U1_ga(distr_in_ggaa(s(X), X))
distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D2, D1)
U1_ga(distr_out_ggaa(DL, DR)) → U2_ga(DR, hbal_tree_in_ga(DL))
U2_ga(DR, hbal_tree_out_ga(L)) → U3_ga(L, hbal_tree_in_ga(DR))
U3_ga(L, hbal_tree_out_ga(R)) → hbal_tree_out_ga(t(x, L, R))
hbal_tree_in_ga(x0)
distr_in_ggaa(x0, x1)
U1_ga(x0)
U2_ga(x0, x1)
U3_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(x1, s(x1)))
U1_GA(distr_out_ggaa(s(z0), s(z0))) → U2_GA(s(z0), hbal_tree_in_ga(s(z0)))
U1_GA(distr_out_ggaa(s(z0), z0)) → U2_GA(z0, hbal_tree_in_ga(s(z0)))
U1_GA(distr_out_ggaa(s(z0), s(z0))) → HBAL_TREE_IN_GA(s(z0))
U1_GA(distr_out_ggaa(s(z0), z0)) → HBAL_TREE_IN_GA(s(z0))
U1_GA(distr_out_ggaa(z0, s(z0))) → HBAL_TREE_IN_GA(z0)
POL(HBAL_TREE_IN_GA(x1)) = x1
POL(U1_GA(x1)) = x1
POL(U1_ga(x1)) = 1 + x1
POL(U2_GA(x1, x2)) = x1
POL(U2_ga(x1, x2)) = 1
POL(U3_ga(x1, x2)) = 1
POL(distr_in_ggaa(x1, x2)) = 0
POL(distr_out_ggaa(x1, x2)) = 1 + x1
POL(hbal_tree_in_ga(x1)) = 1
POL(hbal_tree_out_ga(x1)) = 0
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(t(x1, x2, x3)) = 0
POL(x) = 0
POL(zero) = 0
U2_GA(DR, hbal_tree_out_ga(L)) → HBAL_TREE_IN_GA(DR)
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), s(x1)))
HBAL_TREE_IN_GA(s(s(x1))) → U1_GA(distr_out_ggaa(s(x1), x1))
U1_GA(distr_out_ggaa(z0, s(z0))) → U2_GA(s(z0), hbal_tree_in_ga(z0))
hbal_tree_in_ga(zero) → hbal_tree_out_ga(nil)
hbal_tree_in_ga(s(zero)) → hbal_tree_out_ga(t(x, nil, nil))
hbal_tree_in_ga(s(s(X))) → U1_ga(distr_in_ggaa(s(X), X))
distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D2, D1)
U1_ga(distr_out_ggaa(DL, DR)) → U2_ga(DR, hbal_tree_in_ga(DL))
U2_ga(DR, hbal_tree_out_ga(L)) → U3_ga(L, hbal_tree_in_ga(DR))
U3_ga(L, hbal_tree_out_ga(R)) → hbal_tree_out_ga(t(x, L, R))
hbal_tree_in_ga(x0)
distr_in_ggaa(x0, x1)
U1_ga(x0)
U2_ga(x0, x1)
U3_ga(x0, x1)